R:Realizer. R-Feasible(R)  (es:ES. Consistent(R;es)) 

latex

Definitions	{T}, SQType(T), , x. t(x), t  T, x:A. B(x), P  Q, x:A. B(x), tt, P  Q, if b then t else f fi , ff, False, A, f(x)?z, x(s), P & Q, P  Q
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq, bool cases, not wf, bnot wf, es realizer wf, R-Feasible wf, R-consistent wf, top wf, fpf wf, bool wf, fpf-trivial-subtype-top, R-discrete wf, id-deq wf, product-deq wf, Id wf, fpf-dom wf, assert wf, R-possible-Rconsistent, R-Feasible-possible